\begin{tabbing}
$\forall$$T$:Type, $L$:$T$ List, $P$:($T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. Dec($P$($L$[$x$])))
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P$($L$[$i$]) $\Rightarrow$ $i$$<$$j$ $\Rightarrow$ $P$($L$[$j$]))
\\[0ex]$\Rightarrow$ (\=$\exists$$L_{1}$, $L_{2}$:$T$ List.\+
\\[0ex]$L$ $=$ ($L_{1}$ @ $L_{2}$) \& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$. $\neg$$P$($L_{1}$[$i$])) \& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $P$($L_{2}$[$i$]))
\\[0ex]\& ($\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($x$ $\in$ $L_{2}$)))
\-
\end{tabbing}